The Seventeen Provers of the World, ed. by Freek Wiedijk, foreword by Dana S. Scott, Lecture Notes in Computer Science 3600, Springer, 2006, ISBN 3-540-30704-4. Contains formalized versions of the proof that 2 {\displaystyle {\sqrt {2}}} is irrational in several automated proof systems.
